Nuprl Lemma : decidable-exists-iseg
0,22
postcript
pdf
T
:Type,
P
:((
T
List)
Prop).
(
L
:
T
List. Dec(
P
(
L
)))
(
L
:
T
List. Dec(
L'
:
T
List.
L'
L
&
P
(
L'
)))
latex
Definitions
t
T
,
Prop
,
x
(
s
)
,
x
:
A
.
B
(
x
)
,
Dec(
P
)
,
l1
l2
,
P
&
Q
,
x
:
A
.
B
(
x
)
,
P
Q
,
firstn(
n
;
as
)
,
||
as
||
,
{
i
..
j
}
,
P
Q
,
P
Q
,
i
j
,
False
,
A
,
A
B
,
i
j
<
k
,
Top
,
S
T
,
x
.
t
(
x
)
Lemmas
decidable
functionality
,
decidable
ex
int
seg
,
firstn
is
iseg
,
firstn
append
,
firstn
length
,
top
wf
,
iseg
length
,
non
neg
length
,
iseg
wf
,
int
seg
wf
,
length
wf1
,
firstn
wf
,
decidable
wf
origin